E:Type{i}, T, V:(IdIdType{i}), M:(IdLnkIdType{i}), loc:(EId), kind:(EKnd),
val:(e:Eeventtype(kind;loc;V;M;e)), when, after:(x:Ide:ET(loc(e),x)), time:(E),
sends:(l:IdLnkE(Msg_sub(l;M) List)), sender:({e:E| isrcv(kind(e))} E),
index:(e:{e:E| isrcv(kind(e))} {0..||sends(lnk(kind(e)),sender(e))||}), first:(E),
pred:({e':E| ((first(e')))} E), causl:(EE{i}).
ESAxioms{i:l}
ESAxioms(E; T; M; loc; kind; val; when; after; time; sends; sender; index; first; pred; causl)
 {i'} 

latex

Definitions

t  T, {x:A| B(x)} , Msg_sub(l;M), eventtype(k;loc;V;M;e), f(a), b, x:AB(x), x:A. B(x), isrcv(k), P  Q, lnk(k), ||as||, #$n, {i..j}, i  j , Msg(M), , s = t, Type, A c B, IdLnk, x:A  B(x), x:A. B(x), a < b, , left + right, P  Q, P  Q, type List, [], source(l), Id, A, destination(l), tag(k), msg(l;t;v), S  T, l[i], x,y. t(x;y), SWellFounded(R(x;y)), Trans(T;x,y.E(x;y)), , P & Q, ESAxioms{i:l}(E;T;M;loc;kind;val;when;after;time;sends;sender;index;first;pred;causl), True, T, SqStable(P), Knd, , r - s, r + s, <a, b>, False, act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) )

Lemmas

subtype rel self, true wf, false wf, qadd wf, qsub wf, bool wf, eventtype wf, Knd wf, sq stable from decidable, decidable assert, rationals wf, trans wf, strongwellfounded wf, select wf, Msg wf, msg wf, tagof wf, ldst wf, not wf, Id wf, lsrc wf, iff wf, IdLnk wf, non neg length, int seg wf, length wf1, Msg sub wf, lnk wf, assert wf, isrcv wf